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  2163  3gencl  2838  mob2  2987  moi  2990  reupick3  3494  disjne  3550  elpr2elpr  3864  disji2  4085  tz7.2  4457  funopg  5367  fvun1  5721  fvopab6  5752  isores3  5966  ovmpt4g  6154  ovmpos  6155  ov2gf  6156  ofrval  6255  poxp  6406  smoel  6509  tfr1onlemaccex  6557  tfrcllemaccex  6570  nnaass  6696  qsel  6824  xpdom3m  7061  phpm  7095  ctssdc  7355  mkvprop  7400  prarloclem3  7760  aptisr  8042  axpre-apti  8148  axapti  8292  addn0nid  8595  divvalap  8896  letrp1  9070  p1le  9071  zextle  9615  zextlt  9616  btwnnz  9618  gtndiv  9619  uzind2  9636  fzind  9639  iccleub  10210  uzsubsubfz  10327  elfz0fzfz0  10406  difelfznle  10415  elfzo0le  10470  fzonmapblen  10472  fzofzim  10473  fzosplitprm1  10526  rebtwn2zlemstep  10558  qbtwnxr  10563  icogelb  10571  expcl2lemap  10859  expclzaplem  10871  expnegzap  10881  leexp2r  10901  expnbnd  10971  bcval4  11060  bccmpl  11062  elovmpowrd  11204  ccatval2  11224  ccatrcl1  11240  wrdl1s1  11256  ccat2s1fvwd  11273  swrdsb0eq  11295  swrdccatin1  11355  pfxccatpfx2  11367  absexpzap  11703  divalgb  12549  ndvdssub  12554  dvdsgcd  12646  dfgcd2  12648  rplpwr  12661  nnmindc  12668  lcmgcdlem  12712  coprmdvds1  12726  qredeq  12731  prmdvdsexpr  12785  nnnn0modprm0  12891  pcexp  12945  difsqpwdvds  12974  prmpwdvds  12991  elrestr  13393  isnmgm  13506  grpasscan1  13709  grpinvnz  13717  mulgneg2  13806  dvdsrmul1  14180  dvdsunit  14190  lmodlema  14371  mopni  15276  sincosq1lem  15619  rpcxpmul2  15707  logbgcd1irr  15761  gausslemma2dlem1a  15860  gausslemma2dlem2  15864  gausslemma2dlem4  15866  2lgsoddprmlem3  15913  uhgredgrnv  16062  usgredg4  16139  usgr2v1e2w  16170  uspgr2wlkeqi  16291  eupth2lem3lem4fi  16397