![]() |
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 413 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | exp4b 431 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 206 df-an 397 |
This theorem is referenced by: exp53 448 funssres 6543 fvopab3ig 6942 fvmptt 6966 fvn0elsuppb 8109 tfr3 8342 omordi 8510 odi 8523 nnmordi 8575 php 9151 phpOLD 9163 fiint 9265 ordiso2 9448 cfcoflem 10205 zorn2lem5 10433 inar1 10708 psslinpr 10964 recexsrlem 11036 qaddcl 12887 qmulcl 12889 elfznelfzo 13674 expcan 14071 ltexp2 14072 bernneq 14129 expnbnd 14132 relexpaddg 14935 lcmfunsnlem2lem1 16511 initoeu2lem1 17897 elcls3 22430 opnneissb 22461 txbas 22914 grpoidinvlem3 29346 grporcan 29358 shscli 30157 spansncol 30408 spanunsni 30419 spansncvi 30492 homco1 30641 homulass 30642 atomli 31222 chirredlem1 31230 cdj1i 31273 satffunlem 33886 frinfm 36183 filbcmb 36188 unichnidl 36479 dmncan1 36524 pclfinclN 38402 iccelpart 45595 prmdvdsfmtnof1lem2 45747 scmsuppss 46418 iscnrm3lem4 46939 |
Copyright terms: Public domain | W3C validator |