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  4499  funopg  5411  fvun1  5769  fvopab6  5805  isores3  6021  ovmpt4g  6211  ovmpos  6212  ov2gf  6213  ofrval  6313  poxp  6468  smoel  6571  tfr1onlemaccex  6619  tfrcllemaccex  6632  nnaass  6758  qsel  6886  xpdom3m  7132  phpm  7167  ctssdc  7453  mkvprop  7498  prarloclem3  7864  aptisr  8146  axpre-apti  8252  axapti  8396  addn0nid  8700  divvalap  9004  letrp1  9178  p1le  9179  zextle  9737  zextlt  9738  btwnnz  9740  gtndiv  9741  uzind2  9758  fzind  9761  iccleub  10333  uzsubsubfz  10452  elfz0fzfz0  10533  difelfznle  10542  elfzo0le  10597  fzonmapblen  10599  fzofzim  10600  fzosplitprm1  10653  rebtwn2zlemstep  10687  qbtwnxr  10692  icogelb  10700  expcl2lemap  10988  expclzaplem  11000  expnegzap  11010  leexp2r  11030  expnbnd  11101  bcval4  11190  bccmpl  11192  bcm1n  11207  elovmpowrd  11346  ccatval2  11366  ccatrcl1  11382  wrdl1s1  11398  ccat2s1fvwd  11415  swrdsb0eq  11437  swrdccatin1  11497  pfxccatpfx2  11509  absexpzap  11846  divalgb  12692  ndvdssub  12697  dvdsgcd  12789  dfgcd2  12791  rplpwr  12804  nnmindc  12811  lcmgcdlem  12855  coprmdvds1  12869  qredeq  12874  prmdvdsexpr  12928  nnnn0modprm0  13034  pcexp  13088  difsqpwdvds  13117  prmpwdvds  13134  elrestr  13601  isnmgm  13680  grpasscan1  13868  grpinvnz  13876  mulgneg2  13959  dvdsrmul1  14409  dvdsunit  14419  lmodlema  14628  mopni  15583  sincosq1lem  15926  rpcxpmul2  16015  logbgcd1irr  16069  gausslemma2dlem1a  16177  gausslemma2dlem2  16181  gausslemma2dlem4  16183  2lgsoddprmlem3  16230  uhgredgrnv  16379  usgredg4  16456  usgr2v1e2w  16487  uspgr2wlkeqi  16608  eupth2lem3lem4fi  16714