Theorem exp43 435

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
exp43.1	⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)

Assertion

Ref	Expression
exp43	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Proof of Theorem exp43

Step	Hyp	Ref	Expression
1		exp43.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
2	1	ex 411	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	exp4b 429	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  exp53  446  funssres  6593  fvopab3ig  6995  fvmptt  7019  fvn0elsuppb  8170  tfr3  8403  omordi  8570  odi  8583  nnmordi  8635  php  9214  phpOLD  9226  fiint  9328  ordiso2  9514  cfcoflem  10271  zorn2lem5  10499  inar1  10774  psslinpr  11030  recexsrlem  11102  qaddcl  12955  qmulcl  12957  elfznelfzo  13743  expcan  14140  ltexp2  14141  bernneq  14198  expnbnd  14201  relexpaddg  15006  lcmfunsnlem2lem1  16581  initoeu2lem1  17970  elcls3  22809  opnneissb  22840  txbas  23293  grpoidinvlem3  30024  grporcan  30036  shscli  30835  spansncol  31086  spanunsni  31097  spansncvi  31170  homco1  31319  homulass  31320  atomli  31900  chirredlem1  31908  cdj1i  31951  satffunlem  34688  frinfm  36908  filbcmb  36913  unichnidl  37204  dmncan1  37249  pclfinclN  39126  iccelpart  46401  prmdvdsfmtnof1lem2  46553  scmsuppss  47138  iscnrm3lem4  47658