Theorem ad4antr 768

Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad4antr	|- ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )

Proof of Theorem ad4antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	ad3antrrr 766	. 2 |- ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) -> ps )
3	2	adantr 481	1 |- ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  ad5antr  770  tfrlem1  7472  prdsval  16115  catass  16347  catpropd  16369  cidpropd  16370  subccocl  16505  funcco  16531  natpropd  16636  fucpropd  16637  initoeu2lem1  16664  prfval  16839  xpcpropd  16848  acsfiindd  17177  mhmmnd  17537  scmatscm  20319  cpmatmcllem  20523  mptcoe1matfsupp  20607  mp2pm2mplem4  20614  chpdmatlem2  20644  chfacfisf  20659  chfacfisfcpmat  20660  neitr  20984  hauscmplem  21209  trcfilu  22098  cfilucfil  22364  restmetu  22375  metucn  22376  cnheibor  22754  dvlip2  23758  lgamucov  24764  tgifscgr  25403  iscgrglt  25409  tgbtwnconn1  25470  legtrd  25484  legtri3  25485  legso  25494  hlcgrex  25511  tglndim0  25524  tglinethru  25531  tglnpt2  25536  colline  25544  perpneq  25609  isperp2  25610  footex  25613  opphllem  25627  midex  25629  opphllem3  25641  opphllem5  25643  opphllem6  25644  opphl  25646  outpasch  25647  hlpasch  25648  lnopp2hpgb  25655  hpgerlem  25657  lmieu  25676  trgcopy  25696  cgrahl  25718  acopy  25724  inaghl  25731  cgrg3col4  25734  f1otrg  25751  nbumgrvtx  26242  3cyclfrgr  27152  numclwlk2lem2f1o  27238  omndmul2  29712  isarchi3  29741  archirngz  29743  psgnfzto1stlem  29850  qtophaus  29903  esumcst  30125  sigapildsys  30225  oms0  30359  omssubadd  30362  carsgclctunlem3  30382  eulerpartlemgvv  30438  signsply0  30628  signstfvneq0  30649  actfunsnf1o  30682  reprsuc  30693  reprinfz1  30700  breprexplema  30708  breprexplemc  30710  hgt750lemb  30734  cvmlift3lem2  31302  nn0prpwlem  32317  lindsenlbs  33404  matunitlindflem1  33405  mblfinlem3  33448  mblfinlem4  33449  itg2addnclem2  33462  itg2gt0cn  33465  ftc1cnnc  33484  ftc1anc  33493  sstotbnd2  33573  lcfl8  36791  pell1234qrdich  37425  pell14qrdich  37433  pell1qrgap  37438  pellfundex  37450  cvgdvgrat  38512  infleinflem2  39587  xrralrecnnle  39602  climrec  39835  climsuse  39840  limcrecl  39861  limsupubuz  39945  limsupgtlem  40009  fperdvper  40133  dvnprodlem2  40162  etransclem35  40486  hspmbllem2  40841  smflimlem2  40980  smflimlem4  40982  iccpartgt  41363  sfprmdvdsmersenne  41520  2zlidl  41934  mndpsuppss  42152  ply1mulgsumlem2  42175  nn0sumshdiglemA  42413