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  2771  mob2  2917  moi  2920  reupick3  3420  disjne  3476  disji2  3996  tz7.2  4354  funopg  5250  fvun1  5582  fvopab6  5612  isores3  5815  ovmpt4g  5996  ovmpos  5997  ov2gf  5998  ofrval  6092  poxp  6232  smoel  6300  tfr1onlemaccex  6348  tfrcllemaccex  6361  nnaass  6485  qsel  6611  xpdom3m  6833  phpm  6864  ctssdc  7111  mkvprop  7155  prarloclem3  7495  aptisr  7777  axpre-apti  7883  axapti  8027  addn0nid  8330  divvalap  8630  letrp1  8804  p1le  8805  zextle  9343  zextlt  9344  btwnnz  9346  gtndiv  9347  uzind2  9364  fzind  9367  iccleub  9930  uzsubsubfz  10046  elfz0fzfz0  10125  difelfznle  10134  elfzo0le  10184  fzonmapblen  10186  fzofzim  10187  fzosplitprm1  10233  rebtwn2zlemstep  10252  qbtwnxr  10257  icogelb  10265  expcl2lemap  10531  expclzaplem  10543  expnegzap  10553  leexp2r  10573  expnbnd  10643  bcval4  10731  bccmpl  10733  absexpzap  11088  divalgb  11929  ndvdssub  11934  dvdsgcd  12012  dfgcd2  12014  rplpwr  12027  nnmindc  12034  lcmgcdlem  12076  coprmdvds1  12090  qredeq  12095  prmdvdsexpr  12149  nnnn0modprm0  12254  pcexp  12308  difsqpwdvds  12336  prmpwdvds  12352  elrestr  12695  isnmgm  12778  grpasscan1  12932  grpinvnz  12940  mulgneg2  13015  dvdsrmul1  13269  dvdsunit  13279  lmodlema  13380  mopni  13952  sincosq1lem  14216  logbgcd1irr  14355  2lgsoddprmlem3  14429