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  2835  mob2  2984  moi  2987  reupick3  3490  disjne  3546  elpr2elpr  3857  disji2  4078  tz7.2  4449  funopg  5358  fvun1  5708  fvopab6  5739  isores3  5951  ovmpt4g  6139  ovmpos  6140  ov2gf  6141  ofrval  6241  poxp  6392  smoel  6461  tfr1onlemaccex  6509  tfrcllemaccex  6522  nnaass  6648  qsel  6776  xpdom3m  7013  phpm  7047  ctssdc  7303  mkvprop  7348  prarloclem3  7707  aptisr  7989  axpre-apti  8095  axapti  8240  addn0nid  8543  divvalap  8844  letrp1  9018  p1le  9019  zextle  9561  zextlt  9562  btwnnz  9564  gtndiv  9565  uzind2  9582  fzind  9585  iccleub  10156  uzsubsubfz  10272  elfz0fzfz0  10351  difelfznle  10360  elfzo0le  10414  fzonmapblen  10416  fzofzim  10417  fzosplitprm1  10470  rebtwn2zlemstep  10502  qbtwnxr  10507  icogelb  10515  expcl2lemap  10803  expclzaplem  10815  expnegzap  10825  leexp2r  10845  expnbnd  10915  bcval4  11004  bccmpl  11006  elovmpowrd  11145  ccatval2  11165  ccatrcl1  11181  wrdl1s1  11197  ccat2s1fvwd  11214  swrdsb0eq  11236  swrdccatin1  11296  pfxccatpfx2  11308  absexpzap  11631  divalgb  12476  ndvdssub  12481  dvdsgcd  12573  dfgcd2  12575  rplpwr  12588  nnmindc  12595  lcmgcdlem  12639  coprmdvds1  12653  qredeq  12658  prmdvdsexpr  12712  nnnn0modprm0  12818  pcexp  12872  difsqpwdvds  12901  prmpwdvds  12918  elrestr  13320  isnmgm  13433  grpasscan1  13636  grpinvnz  13644  mulgneg2  13733  dvdsrmul1  14106  dvdsunit  14116  lmodlema  14296  mopni  15196  sincosq1lem  15539  rpcxpmul2  15627  logbgcd1irr  15681  gausslemma2dlem1a  15777  gausslemma2dlem2  15781  gausslemma2dlem4  15783  2lgsoddprmlem3  15830  uhgredgrnv  15977  usgredg4  16054  usgr2v1e2w  16085  uspgr2wlkeqi  16164