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  3674  eqreu  3686  dedth3h  4542  prproe  4832  rbropap  5537  breldmg  5890  ssimaexg  6971  funopdmsn  7154  fpr3g  8306  wfr3g  8340  dfsmo2  8358  omwordri  8583  3ecoptocl  8833  ttrclselem2  9730  frr3g  9763  r1filimi  9906  cfslb  10347  cofsmo  10350  cfsmolem  10351  coftr  10354  domtriomlem  10523  zorn2lem7  10583  ttukey2g  10597  gchi  10712  tskxpss  10860  tskord  10868  infm3  12279  uzind  12794  fzind  12800  fnn0ind  12801  xltnegi  13349  axdc4uz  14130  facwordi  14436  swrdnd2  14809  cshwidxmod  14958  relexpsucl  15189  relexpsucr  15190  relexprelg  15196  relexpaddnn  15209  caubnd  15531  mulgcd  16726  lcmfdvds  16822  lcmfdvdsb  16823  coprmdvds1  16832  pcfac  17082  ramz  17208  imasleval  17718  cictr  17985  initoeu2lem1  18194  drsdir  18481  psasym  18755  pstr  18756  tsrlin  18764  dirge  18782  mgmcl  18824  mgmhmlin  18893  issubmgm2  18897  mhmlin  18993  mhmmulg  19330  issubg2  19357  nsgbi  19372  gsumcom2  20194  srgmulgass  20448  dvdsrtr  20603  rnghmmul  20684  issubrng2  20815  issubrg2  20849  domnmuln0  20966  drnginvrcl  21016  drnginvrn0  21017  drnginvrl  21019  drnginvrr  21020  isdrngd  21027  isdrngdOLD  21029  abvmul  21083  abvtri  21084  lmhmlin  21315  ipcj  21945  cssincl  21999  obsip  22032  decpmatmulsumfsupp  23096  mp2pm2mplem4  23132  pm2mpghm  23139  pm2mpmhmlem1  23141  inopn  23222  basis1  23273  iscldtop  23418  2ndcdisj  23780  cnmpt2t  23997  cnmpt22  23998  cnmptcom  24002  fbasssin  24160  ptcmplem3  24378  xmeteq0  24662  prdsxmslem2  24853  nmvs  25000  nmolb  25041  volfiniun  25873  sincosq1sgn  26832  sincosq2sgn  26833  sincosq3sgn  26834  sincosq4sgn  26835  addsproplem2  28361  negsproplem2  28420  negsid  28432  mulsproplem9  28515  precsexlem10  28607  uzsind  28796  recut  28885  ewlkle  30191  wwlksnext  30487  umgr2adedgwlklem  30538  elwwlks2ons3im  30548  usgrwwlks2on  30552  umgrwwlks2on  30553  conngrv2edg  30801  frgrwopregasn  30922  frgrwopregbsn  30923  frgrwopreglem5  30927  frgrwopreglem5ALT  30928  frgr2wwlkeu  30933  ablocom  31155  nmcvcn  31302  ipassi  31448  htth  31525  shaddcl  31824  shmulcl  31825  shsubcl  31827  chlimi  31841  pjspansn  32184  cnopc  32520  cnfnc  32537  adj1  32540  lnfnmul  32655  atord  32995  atcvat2  32996  cdj3i  33048  nexple  33470  signstfvc  35249  bnj910  35624  bnj1154  35675  acwer1prclem  35815  pconncn  36075  mrsubccat  36369  shftvalg  36589  linethru  37010  sin2h  38626  cos2h  38627  tan2h  38628  dvasin  38715  areacirclem1  38719  riotasv  40109  lsmsatcv  40160  omllaw  40393  2llnjN  40717  dalawlem10  41030  dalawlem13  41033  dalawlem14  41034  pclfinclN  41100  ismrc  43805  fzsplit1nn0  43858  pell1234qrmulcl  43955  pell14qrmulcl  43963  onsucf1olem  44365  iunrelexp0  44795  bi23impib  45562  bi13impib  45563  trelded  45641  suctrALT  45901  suctrALTcf  45997  suctrALTcfVD  45998  stoweidlem17  47120  zm1nn  48465  bgoldbtbndlem4  48999  bgoldbtbnd  49000  tgblthelfgott  49006  vopnbgrelself  49046  clnbgr3stgrgrlic  49211  clcllaw  49381  ztprmneprm  49552  lcoel0  49633  linindslinci  49653  fv2arycl  49853