![]() |
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 633 | 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 197 df-an 385 |
This theorem is referenced by: exp53 648 funssres 6091 fvopab3ig 6440 fvmptt 6462 fvn0elsuppb 7480 tfr3 7664 omordi 7815 odi 7828 nnmordi 7880 php 8309 fiint 8402 ordiso2 8585 cfcoflem 9286 zorn2lem5 9514 inar1 9789 psslinpr 10045 recexsrlem 10116 qaddcl 11997 qmulcl 11999 elfznelfzo 12767 expcan 13107 ltexp2 13108 bernneq 13184 expnbnd 13187 relexpaddg 13992 lcmfunsnlem2lem1 15553 initoeu2lem1 16865 elcls3 21089 opnneissb 21120 txbas 21572 grpoidinvlem3 27669 grporcan 27681 shscli 28485 spansncol 28736 spanunsni 28747 spansncvi 28820 homco1 28969 homulass 28970 atomli 29550 chirredlem1 29558 cdj1i 29601 frinfm 33843 filbcmb 33848 unichnidl 34143 dmncan1 34188 pclfinclN 35739 iccelpart 41879 prmdvdsfmtnof1lem2 42007 scmsuppss 42663 |
Copyright terms: Public domain | W3C validator |