Theorem 3impia 1231

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mopick2  2170  3gencl  2856  mob2  3006  moi  3009  reupick3  3518  disjne  3578  elpr2elpr  3901  disji2  4122  tz7.2  4501  funopg  5414  fvun1  5772  fvopab6  5808  isores3  6024  ovmpt4g  6214  ovmpos  6215  ov2gf  6216  ofrval  6317  poxp  6472  smoel  6575  tfr1onlemaccex  6623  tfrcllemaccex  6636  nnaass  6762  qsel  6890  xpdom3m  7136  phpm  7171  ctssdc  7459  mkvprop  7504  prarloclem3  7870  aptisr  8152  axpre-apti  8258  axapti  8402  addn0nid  8707  divvalap  9012  letrp1  9186  p1le  9187  zextle  9748  zextlt  9749  btwnnz  9751  gtndiv  9752  uzind2  9769  fzind  9772  iccleub  10350  uzsubsubfz  10469  elfz0fzfz0  10550  difelfznle  10559  elfzo0le  10614  fzonmapblen  10616  fzofzim  10617  fzosplitprm1  10670  rebtwn2zlemstep  10704  qbtwnxr  10709  icogelb  10717  expcl2lemap  11009  expclzaplem  11021  expnegzap  11031  leexp2r  11051  expnbnd  11122  bcval4  11212  bccmpl  11214  bcm1n  11229  elovmpowrd  11368  ccatval2  11388  ccatrcl1  11404  wrdl1s1  11420  ccat2s1fvwd  11437  swrdsb0eq  11459  swrdccatin1  11519  pfxccatpfx2  11531  absexpzap  11869  divalgb  12717  ndvdssub  12722  dvdsgcd  12814  dfgcd2  12816  rplpwr  12829  nnmindc  12836  lcmgcdlem  12880  coprmdvds1  12894  qredeq  12899  prmdvdsexpr  12954  nnnn0modprm0  13063  pcexp  13117  difsqpwdvds  13146  prmpwdvds  13163  elrestr  13660  isnmgm  13739  grpasscan1  13927  grpinvnz  13935  mulgneg2  14018  dvdsrmul1  14518  dvdsunit  14528  lmodlema  14737  mopni  15708  sincosq1lem  16052  rpcxpmul2  16146  rpcxpmul2z  16148  logbgcd1irr  16203  bcmono  16304  gausslemma2dlem1a  16382  gausslemma2dlem2  16386  gausslemma2dlem4  16388  2lgsoddprmlem3  16435  uhgredgrnv  16584  usgredg4  16661  usgr2v1e2w  16692  uspgr2wlkeqi  16813  eupth2lem3lem4fi  16919