Theorem 3impa 1218

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

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

Assertion

Ref	Expression
3impa	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impa

Step	Hyp	Ref	Expression
1		3impa.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
2	1	exp31 364	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1217	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002

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 1004

This theorem is referenced by:  ex3  1219  3impdir  1328  syl3an9b  1344  biimp3a  1379  stoic3  1473  rspec3  2620  rspc3v  2923  raltpg  3719  rextpg  3720  disjiun  4077  otexg  4315  opelopabt  4349  tpexg  4534  3optocl  4796  fun2ssres  5360  funssfv  5652  fvun1  5699  foco2  5876  f1elima  5896  eloprabga  6090  caovimo  6198  ot1stg  6296  ot2ndg  6297  ot3rdgg  6298  brtposg  6398  rdgexggg  6521  rdgivallem  6525  nnmass  6631  nndir  6634  nnaword  6655  th3q  6785  ecovass  6789  ecoviass  6790  fpmg  6819  findcard  7046  unfiin  7084  pr1or2  7363  addasspig  7513  mulasspig  7515  mulcanpig  7518  ltapig  7521  ltmpig  7522  addassnqg  7565  ltbtwnnqq  7598  mulnnnq0  7633  addassnq0  7645  genpassl  7707  genpassu  7708  genpassg  7709  aptiprleml  7822  adddir  8133  le2tri3i  8251  addsub12  8355  subdir  8528  reapmul1  8738  recexaplem2  8795  div12ap  8837  divdiv32ap  8863  divdivap1  8866  lble  9090  zaddcllemneg  9481  fnn0ind  9559  xrltso  9988  iccgelb  10124  elicc4  10132  elfz  10206  fzrevral  10297  expnegap0  10764  expgt0  10789  expge0  10792  expge1  10793  mulexpzap  10796  expp1zap  10805  expm1ap  10806  apexp1  10935  ccatsymb  11132  abssubap0  11596  binom  11990  dvds0lem  12307  dvdsnegb  12314  muldvds1  12322  muldvds2  12323  divalgmodcl  12434  gcd2n0cl  12485  lcmdvds  12596  prmdvdsexp  12665  rpexp1i  12671  eqglact  13757  lss0cl  14327  cnpval  14866  cnf2  14873  cnnei  14900  blssec  15106  blpnfctr  15107  mopni2  15151  mopni3  15152  dvply1  15433  uhgrm  15872  upgrm  15894  upgr1or2  15895