Theorem 3exp 1204

Description: Exportation inference. (Contributed by NM, 30-May-1994.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3exp	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem 3exp

Step	Hyp	Ref	Expression
1		pm3.2an3 1178	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 ∧ 𝜓 ∧ 𝜒))))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl8 71	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  3expa  1205  3expb  1206  3expia  1207  3expib  1208  3com23  1211  3an1rs  1221  3exp1  1225  3expd  1226  exp5o  1228  syl3an2  1283  syl3an3  1284  syl2an23an  1311  3impexpbicomi  1458  rexlimdv3a  2624  rabssdv  3272  reupick2  3458  ssorduni  4534  tfisi  4634  fvssunirng  5590  f1oiso2  5895  poxp  6317  tfrlem5  6399  nndi  6571  nnmass  6572  findcard  6984  ac6sfi  6994  mulcanpig  7447  divgt0  8944  divge0  8945  uzind  9483  uzind2  9484  facavg  10889  prodfap0  11798  prodfrecap  11799  fprodabs  11869  dvdsmodexp  12048  dvdsaddre2b  12094  dvdsnprmd  12389  prmndvdsfaclt  12420  fermltl  12498  pceu  12560  mulgass2  13762  islss4  14086  rnglidlmcl  14184  fiinopn  14418  neipsm  14568  tpnei  14574  opnneiid  14578  neibl  14905  tgqioo  14969  gausslemma2dlem1a  15477