Theorem 3impia 1227

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 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:  mopick2  2166  3gencl  2850  mob2  3000  moi  3003  reupick3  3510  disjne  3566  elpr2elpr  3885  disji2  4106  tz7.2  4480  funopg  5391  fvun1  5748  fvopab6  5779  isores3  5994  ovmpt4g  6184  ovmpos  6185  ov2gf  6186  ofrval  6286  poxp  6441  smoel  6544  tfr1onlemaccex  6592  tfrcllemaccex  6605  nnaass  6731  qsel  6859  xpdom3m  7098  phpm  7133  ctssdc  7417  mkvprop  7462  prarloclem3  7828  aptisr  8110  axpre-apti  8216  axapti  8360  addn0nid  8663  divvalap  8965  letrp1  9139  p1le  9140  zextle  9687  zextlt  9688  btwnnz  9690  gtndiv  9691  uzind2  9708  fzind  9711  iccleub  10283  uzsubsubfz  10401  elfz0fzfz0  10482  difelfznle  10491  elfzo0le  10546  fzonmapblen  10548  fzofzim  10549  fzosplitprm1  10602  rebtwn2zlemstep  10636  qbtwnxr  10641  icogelb  10649  expcl2lemap  10937  expclzaplem  10949  expnegzap  10959  leexp2r  10979  expnbnd  11050  bcval4  11139  bccmpl  11141  bcm1n  11156  elovmpowrd  11291  ccatval2  11311  ccatrcl1  11327  wrdl1s1  11343  ccat2s1fvwd  11360  swrdsb0eq  11382  swrdccatin1  11442  pfxccatpfx2  11454  absexpzap  11790  divalgb  12636  ndvdssub  12641  dvdsgcd  12733  dfgcd2  12735  rplpwr  12748  nnmindc  12755  lcmgcdlem  12799  coprmdvds1  12813  qredeq  12818  prmdvdsexpr  12872  nnnn0modprm0  12978  pcexp  13032  difsqpwdvds  13061  prmpwdvds  13078  elrestr  13544  isnmgm  13623  grpasscan1  13818  grpinvnz  13826  mulgneg2  13909  dvdsrmul1  14347  dvdsunit  14357  lmodlema  14566  mopni  15473  sincosq1lem  15816  rpcxpmul2  15904  logbgcd1irr  15958  gausslemma2dlem1a  16057  gausslemma2dlem2  16061  gausslemma2dlem4  16063  2lgsoddprmlem3  16110  uhgredgrnv  16259  usgredg4  16336  usgr2v1e2w  16367  uspgr2wlkeqi  16488  eupth2lem3lem4fi  16594