Theorem 3impia 1200

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 115	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1193	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 980

This theorem is referenced by:  mopick2  2109  3gencl  2773  mob2  2919  moi  2922  reupick3  3422  disjne  3478  disji2  3998  tz7.2  4356  funopg  5252  fvun1  5584  fvopab6  5614  isores3  5818  ovmpt4g  5999  ovmpos  6000  ov2gf  6001  ofrval  6095  poxp  6235  smoel  6303  tfr1onlemaccex  6351  tfrcllemaccex  6364  nnaass  6488  qsel  6614  xpdom3m  6836  phpm  6867  ctssdc  7114  mkvprop  7158  prarloclem3  7498  aptisr  7780  axpre-apti  7886  axapti  8030  addn0nid  8333  divvalap  8633  letrp1  8807  p1le  8808  zextle  9346  zextlt  9347  btwnnz  9349  gtndiv  9350  uzind2  9367  fzind  9370  iccleub  9933  uzsubsubfz  10049  elfz0fzfz0  10128  difelfznle  10137  elfzo0le  10187  fzonmapblen  10189  fzofzim  10190  fzosplitprm1  10236  rebtwn2zlemstep  10255  qbtwnxr  10260  icogelb  10268  expcl2lemap  10534  expclzaplem  10546  expnegzap  10556  leexp2r  10576  expnbnd  10646  bcval4  10734  bccmpl  10736  absexpzap  11091  divalgb  11932  ndvdssub  11937  dvdsgcd  12015  dfgcd2  12017  rplpwr  12030  nnmindc  12037  lcmgcdlem  12079  coprmdvds1  12093  qredeq  12098  prmdvdsexpr  12152  nnnn0modprm0  12257  pcexp  12311  difsqpwdvds  12339  prmpwdvds  12355  elrestr  12701  isnmgm  12784  grpasscan1  12938  grpinvnz  12946  mulgneg2  13022  dvdsrmul1  13276  dvdsunit  13286  lmodlema  13387  mopni  14021  sincosq1lem  14285  logbgcd1irr  14424  2lgsoddprmlem3  14498