Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > exp43 | Structured version Visualization version GIF version |
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
exp43.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) |
Ref | Expression |
---|---|
exp43 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp43.1 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
2 | 1 | ex 449 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | exp4b 630 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 df-an 385 |
This theorem is referenced by: exp53 645 funssres 5844 fvopab3ig 6188 fvmptt 6208 fvn0elsuppb 7199 tfr3 7382 omordi 7533 odi 7546 nnmordi 7598 php 8029 fiint 8122 ordiso2 8303 cfcoflem 8977 zorn2lem5 9205 inar1 9476 psslinpr 9732 recexsrlem 9803 qaddcl 11680 qmulcl 11682 elfznelfzo 12439 expcan 12775 ltexp2 12776 bernneq 12852 expnbnd 12855 relexpaddg 13641 lcmfunsnlem2lem1 15189 initoeu2lem1 16487 elcls3 20697 opnneissb 20728 txbas 21180 grpoidinvlem3 26744 grporcan 26756 shscli 27560 spansncol 27811 spanunsni 27822 spansncvi 27895 homco1 28044 homulass 28045 atomli 28625 chirredlem1 28633 cdj1i 28676 frinfm 32700 filbcmb 32705 unichnidl 33000 dmncan1 33045 pclfinclN 34254 iccelpart 39971 prmdvdsfmtnof1lem2 40035 scmsuppss 41947 |
Copyright terms: Public domain | W3C validator |