Theorem 3impia 1226

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

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

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 1006

This theorem is referenced by:  mopick2  2163  3gencl  2837  mob2  2986  moi  2989  reupick3  3492  disjne  3548  elpr2elpr  3859  disji2  4080  tz7.2  4451  funopg  5360  fvun1  5712  fvopab6  5743  isores3  5955  ovmpt4g  6143  ovmpos  6144  ov2gf  6145  ofrval  6245  poxp  6396  smoel  6465  tfr1onlemaccex  6513  tfrcllemaccex  6526  nnaass  6652  qsel  6780  xpdom3m  7017  phpm  7051  ctssdc  7311  mkvprop  7356  prarloclem3  7716  aptisr  7998  axpre-apti  8104  axapti  8249  addn0nid  8552  divvalap  8853  letrp1  9027  p1le  9028  zextle  9570  zextlt  9571  btwnnz  9573  gtndiv  9574  uzind2  9591  fzind  9594  iccleub  10165  uzsubsubfz  10281  elfz0fzfz0  10360  difelfznle  10369  elfzo0le  10423  fzonmapblen  10425  fzofzim  10426  fzosplitprm1  10479  rebtwn2zlemstep  10511  qbtwnxr  10516  icogelb  10524  expcl2lemap  10812  expclzaplem  10824  expnegzap  10834  leexp2r  10854  expnbnd  10924  bcval4  11013  bccmpl  11015  elovmpowrd  11154  ccatval2  11174  ccatrcl1  11190  wrdl1s1  11206  ccat2s1fvwd  11223  swrdsb0eq  11245  swrdccatin1  11305  pfxccatpfx2  11317  absexpzap  11640  divalgb  12485  ndvdssub  12490  dvdsgcd  12582  dfgcd2  12584  rplpwr  12597  nnmindc  12604  lcmgcdlem  12648  coprmdvds1  12662  qredeq  12667  prmdvdsexpr  12721  nnnn0modprm0  12827  pcexp  12881  difsqpwdvds  12910  prmpwdvds  12927  elrestr  13329  isnmgm  13442  grpasscan1  13645  grpinvnz  13653  mulgneg2  13742  dvdsrmul1  14115  dvdsunit  14125  lmodlema  14305  mopni  15205  sincosq1lem  15548  rpcxpmul2  15636  logbgcd1irr  15690  gausslemma2dlem1a  15786  gausslemma2dlem2  15790  gausslemma2dlem4  15792  2lgsoddprmlem3  15839  uhgredgrnv  15988  usgredg4  16065  usgr2v1e2w  16096  uspgr2wlkeqi  16217