Theorem 3impa 1221

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 1220	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 1007

This theorem is referenced by:  ex3  1222  3impdir  1331  syl3an9b  1347  biimp3a  1382  stoic3  1476  rspec3  2632  rspc3v  2937  raltpg  3742  rextpg  3743  disjiun  4104  otexg  4346  opelopabt  4380  tpexg  4565  3optocl  4828  fun2ssres  5396  funssfv  5696  fvun1  5743  foco2  5926  f1elima  5946  eloprabga  6140  caovimo  6248  ot1stg  6346  ot2ndg  6347  ot3rdgg  6348  brtposg  6485  rdgexggg  6608  rdgivallem  6612  nnmass  6720  nndir  6723  nnaword  6744  th3q  6874  ecovass  6878  ecoviass  6879  fpmg  6908  findcard  7145  unfiin  7186  pr1or2  7491  addasspig  7645  mulasspig  7647  mulcanpig  7650  ltapig  7653  ltmpig  7654  addassnqg  7697  ltbtwnnqq  7730  mulnnnq0  7765  addassnq0  7777  genpassl  7839  genpassu  7840  genpassg  7841  aptiprleml  7954  adddir  8265  le2tri3i  8382  addsub12  8486  subdir  8659  reapmul1  8869  recexaplem2  8926  div12ap  8968  divdiv32ap  8994  divdivap1  8997  lble  9221  zaddcllemneg  9616  fnn0ind  9694  xrltso  10129  iccgelb  10265  elicc4  10273  elfz  10348  fzrevral  10439  expnegap0  10909  expgt0  10934  expge0  10937  expge1  10938  mulexpzap  10941  expp1zap  10950  expm1ap  10951  apexp1  11080  ccatsymb  11290  abssubap0  11775  binom  12170  dvds0lem  12487  dvdsnegb  12494  muldvds1  12502  muldvds2  12503  divalgmodcl  12614  gcd2n0cl  12665  lcmdvds  12776  prmdvdsexp  12845  rpexp1i  12851  eqglact  13942  lss0cl  14517  cnpval  15063  cnf2  15070  cnnei  15097  blssec  15303  blpnfctr  15304  mopni2  15348  mopni3  15349  dvply1  15630  uhgrm  16073  upgrm  16095  upgr1or2  16096