Theorem 3impib 1105

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 406	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1098	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 199  df-an 387  df-3an 1073

This theorem is referenced by:  3impia  1106  mob  3600  eqreu  3610  dedth3h  4365  prproe  4669  rbropap  5253  breldmg  5575  ssimaexg  6524  funopdmsn  6681  wfr3g  7695  dfsmo2  7727  omwordri  7936  3ecoptocl  8122  cfslb  9423  cofsmo  9426  cfsmolem  9427  coftr  9430  domtriomlem  9599  zorn2lem7  9659  ttukey2g  9673  gchi  9781  tskxpss  9929  tskord  9937  infm3  11336  uzind  11821  fzind  11827  fnn0ind  11828  xltnegi  12359  axdc4uz  13102  facwordi  13394  swrdnd2  13750  cshwidxmod  13954  relexpsucr  14176  relexpsucl  14180  relexprelg  14185  relexpaddnn  14198  caubnd  14505  mulgcd  15671  lcmfdvds  15761  lcmfdvdsb  15762  coprmdvds1  15771  pcfac  16007  ramz  16133  imasleval  16587  cictr  16850  initoeu2lem1  17049  drsdir  17321  psasym  17596  pstr  17597  tsrlin  17605  dirge  17623  mgmcl  17631  mhmlin  17728  mhmmulg  17967  issubg2  17993  nsgbi  18009  cygabl  18678  gsumcom2  18760  srgmulgass  18918  dvdsrtr  19039  drnginvrcl  19156  drnginvrn0  19157  drnginvrl  19158  drnginvrr  19159  isdrngd  19164  issubrg2  19192  abvmul  19221  abvtri  19222  lmhmlin  19430  domnmuln0  19695  ipcj  20377  cssincl  20431  obsip  20464  decpmatmulsumfsupp  20985  mp2pm2mplem4  21021  pm2mpghm  21028  pm2mpmhmlem1  21030  inopn  21111  basis1  21162  iscldtop  21307  2ndcdisj  21668  cnmpt2t  21885  cnmpt22  21886  cnmptcom  21890  fbasssin  22048  ptcmplem3  22266  xmeteq0  22551  prdsxmslem2  22742  nmvs  22888  nmolb  22929  volfiniun  23751  sincosq1sgn  24688  sincosq2sgn  24689  sincosq3sgn  24690  sincosq4sgn  24691  ewlkle  26953  wwlksnext  27254  umgr2adedgwlklem  27324  elwwlks2ons3im  27334  umgrwwlks2on  27337  conngrv2edg  27598  frgrwopregasn  27724  frgrwopregbsn  27725  frgrwopreglem5  27729  frgrwopreglem5ALT  27730  frgr2wwlkeu  27735  ablocom  27975  nmcvcn  28122  ipassi  28268  htth  28347  shaddcl  28646  shmulcl  28647  shsubcl  28649  chlimi  28663  pjspansn  29008  cnopc  29344  cnfnc  29361  adj1  29364  lnfnmul  29479  atord  29819  atcvat2  29820  cdj3i  29872  nexple  30669  signstfvc  31252  bnj910  31617  bnj1154  31666  pconncn  31805  mrsubccat  32014  shftvalg  32211  frr3g  32368  frrlem5e  32377  linethru  32849  sin2h  34026  cos2h  34027  tan2h  34028  dvasin  34123  areacirclem1  34127  riotasv  35115  lsmsatcv  35166  omllaw  35399  2llnjN  35723  dalawlem10  36036  dalawlem13  36039  dalawlem14  36040  pclfinclN  36106  ismrc  38228  fzsplit1nn0  38281  pell1234qrmulcl  38383  pell14qrmulcl  38391  iunrelexp0  38955  bi23impib  39649  bi13impib  39650  trelded  39729  suctrALT  39999  suctrALTcf  40095  suctrALTcfVD  40096  stoweidlem17  41165  zm1nn  42348  bgoldbtbndlem4  42725  bgoldbtbnd  42726  tgblthelfgott  42732  mgmhmlin  42805  issubmgm2  42809  clcllaw  42846  rnghmmul  42919  ztprmneprm  43144  lcoel0  43236  linindslinci  43256