| 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 412 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
| 3 | 2 | exp4b 430 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: exp53 447 funssres 6610 fvopab3ig 7012 fvmptt 7036 fvn0elsuppb 8206 tfr3 8439 omordi 8604 odi 8617 nnmordi 8669 php 9247 phpOLD 9259 fiint 9366 fiintOLD 9367 ordiso2 9555 cfcoflem 10312 zorn2lem5 10540 inar1 10815 psslinpr 11071 recexsrlem 11143 qaddcl 13007 qmulcl 13009 elfznelfzo 13811 expcan 14209 ltexp2 14210 bernneq 14268 expnbnd 14271 relexpaddg 15092 lcmfunsnlem2lem1 16675 initoeu2lem1 18059 elcls3 23091 opnneissb 23122 txbas 23575 grpoidinvlem3 30525 grporcan 30537 shscli 31336 spansncol 31587 spanunsni 31598 spansncvi 31671 homco1 31820 homulass 31821 atomli 32401 chirredlem1 32409 cdj1i 32452 satffunlem 35406 frinfm 37742 filbcmb 37747 unichnidl 38038 dmncan1 38083 pclfinclN 39952 iccelpart 47420 prmdvdsfmtnof1lem2 47572 gpgcubic 48035 gpg5nbgr3star 48037 scmsuppss 48287 iscnrm3lem4 48833 |
| Copyright terms: Public domain | W3C validator |