Theorem 3impia 1224

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 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:  mopick2  2161  3gencl  2834  mob2  2983  moi  2986  reupick3  3489  disjne  3545  elpr2elpr  3854  disji2  4075  tz7.2  4445  funopg  5352  fvun1  5702  fvopab6  5733  isores3  5945  ovmpt4g  6133  ovmpos  6134  ov2gf  6135  ofrval  6235  poxp  6384  smoel  6452  tfr1onlemaccex  6500  tfrcllemaccex  6513  nnaass  6639  qsel  6767  xpdom3m  7001  phpm  7035  ctssdc  7291  mkvprop  7336  prarloclem3  7695  aptisr  7977  axpre-apti  8083  axapti  8228  addn0nid  8531  divvalap  8832  letrp1  9006  p1le  9007  zextle  9549  zextlt  9550  btwnnz  9552  gtndiv  9553  uzind2  9570  fzind  9573  iccleub  10139  uzsubsubfz  10255  elfz0fzfz0  10334  difelfznle  10343  elfzo0le  10397  fzonmapblen  10399  fzofzim  10400  fzosplitprm1  10452  rebtwn2zlemstep  10484  qbtwnxr  10489  icogelb  10497  expcl2lemap  10785  expclzaplem  10797  expnegzap  10807  leexp2r  10827  expnbnd  10897  bcval4  10986  bccmpl  10988  elovmpowrd  11126  ccatval2  11146  ccatrcl1  11162  wrdl1s1  11178  swrdsb0eq  11212  swrdccatin1  11272  pfxccatpfx2  11284  absexpzap  11606  divalgb  12451  ndvdssub  12456  dvdsgcd  12548  dfgcd2  12550  rplpwr  12563  nnmindc  12570  lcmgcdlem  12614  coprmdvds1  12628  qredeq  12633  prmdvdsexpr  12687  nnnn0modprm0  12793  pcexp  12847  difsqpwdvds  12876  prmpwdvds  12893  elrestr  13295  isnmgm  13408  grpasscan1  13611  grpinvnz  13619  mulgneg2  13708  dvdsrmul1  14081  dvdsunit  14091  lmodlema  14271  mopni  15171  sincosq1lem  15514  rpcxpmul2  15602  logbgcd1irr  15656  gausslemma2dlem1a  15752  gausslemma2dlem2  15756  gausslemma2dlem4  15758  2lgsoddprmlem3  15805  uhgredgrnv  15951  usgredg4  16028  uspgr2wlkeqi  16108