Theorem 3impib 1134

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

Ref	Expression
3impib.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
3impib	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impib

Step	Hyp	Ref	Expression
1		3impib.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 421	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1128	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3impia  1135  mob  3683  eqreu  3695  dedth3h  4553  prproe  4875  rbropap  5553  breldmg  5904  ssimaexg  6974  funopdmsn  7154  fpr3g  8291  wfr3g  8325  dfsmo2  8343  omwordri  8566  3ecoptocl  8816  ttrclselem2  9705  frr3g  9738  cfslb  10268  cofsmo  10271  cfsmolem  10272  coftr  10275  domtriomlem  10444  zorn2lem7  10504  ttukey2g  10518  gchi  10627  tskxpss  10775  tskord  10783  infm3  12192  uzind  12706  fzind  12712  fnn0ind  12713  xltnegi  13260  axdc4uz  14040  facwordi  14345  swrdnd2  14717  cshwidxmod  14866  relexpsucl  15094  relexpsucr  15095  relexprelg  15101  relexpaddnn  15114  caubnd  15436  mulgcd  16631  lcmfdvds  16725  lcmfdvdsb  16726  coprmdvds1  16735  pcfac  16984  ramz  17110  imasleval  17620  cictr  17887  initoeu2lem1  18096  drsdir  18383  psasym  18657  pstr  18658  tsrlin  18666  dirge  18684  mgmcl  18726  mgmhmlin  18786  issubmgm2  18790  mhmlin  18882  mhmmulg  19212  issubg2  19239  nsgbi  19254  gsumcom2  20076  srgmulgass  20330  dvdsrtr  20483  rnghmmul  20564  issubrng2  20694  issubrg2  20728  domnmuln0  20845  drnginvrcl  20894  drnginvrn0  20895  drnginvrl  20897  drnginvrr  20898  isdrngd  20905  isdrngdOLD  20907  abvmul  20961  abvtri  20962  lmhmlin  21193  ipcj  21821  cssincl  21875  obsip  21908  decpmatmulsumfsupp  22967  mp2pm2mplem4  23003  pm2mpghm  23010  pm2mpmhmlem1  23012  inopn  23093  basis1  23144  iscldtop  23289  2ndcdisj  23650  cnmpt2t  23867  cnmpt22  23868  cnmptcom  23872  fbasssin  24030  ptcmplem3  24248  xmeteq0  24532  prdsxmslem2  24723  nmvs  24870  nmolb  24911  volfiniun  25743  sincosq1sgn  26700  sincosq2sgn  26701  sincosq3sgn  26702  sincosq4sgn  26703  addsproplem2  28200  negsproplem2  28259  negsid  28271  mulsproplem9  28354  precsexlem10  28446  uzsind  28635  recut  28724  ewlkle  29992  wwlksnext  30279  umgr2adedgwlklem  30330  elwwlks2ons3im  30340  usgrwwlks2on  30344  umgrwwlks2on  30345  conngrv2edg  30583  frgrwopregasn  30704  frgrwopregbsn  30705  frgrwopreglem5  30709  frgrwopreglem5ALT  30710  frgr2wwlkeu  30715  ablocom  30937  nmcvcn  31084  ipassi  31230  htth  31307  shaddcl  31606  shmulcl  31607  shsubcl  31609  chlimi  31623  pjspansn  31966  cnopc  32302  cnfnc  32319  adj1  32322  lnfnmul  32437  atord  32777  atcvat2  32778  cdj3i  32830  nexple  33214  signstfvc  34992  bnj910  35367  bnj1154  35418  r1filimi  35521  umgr2cycllem  35652  pconncn  35736  mrsubccat  36030  shftvalg  36244  linethru  36665  sin2h  38301  cos2h  38302  tan2h  38303  dvasin  38395  areacirclem1  38399  riotasv  39773  lsmsatcv  39824  omllaw  40057  2llnjN  40381  dalawlem10  40694  dalawlem13  40697  dalawlem14  40698  pclfinclN  40764  ismrc  43472  fzsplit1nn0  43525  pell1234qrmulcl  43622  pell14qrmulcl  43630  onsucf1olem  44037  iunrelexp0  44468  bi23impib  45235  bi13impib  45236  trelded  45314  suctrALT  45574  suctrALTcf  45670  suctrALTcfVD  45671  stoweidlem17  46771  zm1nn  48079  bgoldbtbndlem4  48613  bgoldbtbnd  48614  tgblthelfgott  48620  vopnbgrelself  48660  clnbgr3stgrgrlic  48825  clcllaw  48996  ztprmneprm  49167  lcoel0  49248  linindslinci  49268  fv2arycl  49468