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  6576  tfr1onlemaccex  6624  tfrcllemaccex  6637  nnaass  6763  qsel  6891  xpdom3m  7138  phpm  7173  ctssdc  7459  mkvprop  7504  prarloclem3  7870  aptisr  8152  axpre-apti  8258  axapti  8402  addn0nid  8707  divvalap  9012  letrp1  9186  p1le  9187  zextle  9747  zextlt  9748  btwnnz  9750  gtndiv  9751  uzind2  9768  fzind  9771  iccleub  10349  uzsubsubfz  10468  elfz0fzfz0  10549  difelfznle  10558  elfzo0le  10613  fzonmapblen  10615  fzofzim  10616  fzosplitprm1  10669  rebtwn2zlemstep  10703  qbtwnxr  10708  icogelb  10716  expcl2lemap  11008  expclzaplem  11020  expnegzap  11030  leexp2r  11050  expnbnd  11121  bcval4  11211  bccmpl  11213  bcm1n  11228  elovmpowrd  11367  ccatval2  11387  ccatrcl1  11403  wrdl1s1  11419  ccat2s1fvwd  11436  swrdsb0eq  11458  swrdccatin1  11518  pfxccatpfx2  11530  absexpzap  11868  divalgb  12716  ndvdssub  12721  dvdsgcd  12813  dfgcd2  12815  rplpwr  12828  nnmindc  12835  lcmgcdlem  12879  coprmdvds1  12893  qredeq  12898  prmdvdsexpr  12953  nnnn0modprm0  13062  pcexp  13116  difsqpwdvds  13145  prmpwdvds  13162  elrestr  13659  isnmgm  13738  grpasscan1  13926  grpinvnz  13934  mulgneg2  14017  dvdsrmul1  14517  dvdsunit  14527  lmodlema  14736  mopni  15725  sincosq1lem  16069  rpcxpmul2  16163  rpcxpmul2z  16165  logbgcd1irr  16220  bcmono  16321  gausslemma2dlem1a  16399  gausslemma2dlem2  16403  gausslemma2dlem4  16405  2lgsoddprmlem3  16452  uhgredgrnv  16601  usgredg4  16678  usgr2v1e2w  16709  uspgr2wlkeqi  16830  eupth2lem3lem4fi  16936