Theorem adantrd 491

Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)

Hypothesis

Ref	Expression
adantrd.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
adantrd	⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

Proof of Theorem adantrd

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adantrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  im2anan9  620  jaoa  957  prlem1  1054  cad0  1618  dfsb1  2479  unineq  4251  dfopif  4834  elssabg  5298  exopxfr2  5808  tz7.7  6358  oneqmini  6385  fvun1  6952  fconst5  7180  fpropnf1  7242  f1ounsn  7247  isomin  7312  isofrlem  7315  poxp  8107  poseq  8137  tposfo2  8228  onfununi  8310  tfrlem9a  8354  oecl  8501  oawordri  8514  omwordri  8536  odi  8543  pssnn  9132  prdom2  9959  acni2  9999  cardinfima  10050  cfslb2n  10221  infpssrlem4  10259  axdc3lem4  10406  brdom6disj  10485  tskr1om  10720  indpi  10860  1idpr  10982  1re  11174  mulge0  11696  infm3  12142  uzind  12626  suprfinzcl  12648  uzwo  12870  xrlttr  13100  xmullem2  13225  snunico  13440  fzen  13502  fz0fzelfz0  13595  sqlecan  14174  hashf1lem2  14421  ccatsymb  14547  lo1le  15618  fsumss  15691  ntrivcvgfvn0  15865  fprodss  15914  smupvallem  16453  zeqzmulgcd  16480  lcmgcdlem  16576  lcmdvds  16578  lcmfunsnlem2lem1  16608  coprmproddvdslem  16632  cncongr2  16638  exprmfct  16674  infpnlem1  16881  prmdvdsprmop  17014  prmgaplem7  17028  prmlem0  17076  sscfn2  17780  isssc  17782  iszeroi  17971  funcsetcestrclem8  18123  dirge  18562  efgval  19647  dmdprd  19930  dprdw  19942  rhmsubclem4  20597  lpigen  21245  psrbaglefi  21835  matvscl  22318  scmatghm  22420  slesolinv  22567  cpmatacl  22603  pnfnei  23107  mnfnei  23108  cmpcld  23289  isfildlem  23744  metrest  24412  blval2  24450  iscmet3lem2  25192  ivthlem3  25354  mbfi1fseqlem4  25619  itg2seq  25643  aalioulem6  26245  taylthlem2  26282  chpchtsum  27130  dchrmulcl  27160  bcmono  27188  nosupno  27615  nosupbday  27617  noinfno  27630  noinfbday  27632  nocvxminlem  27689  cuteq1  27746  onscutlt  28165  onsiso  28169  bdayn0p1  28258  zs12ge0  28342  cgrg3col4  28780  brbtwn2  28832  axeuclid  28890  umgredg  29065  pthdivtx  29657  pthdlem1  29696  shsvs  31252  cnlnssadj  32009  atexch  32310  mdsymlem5  32336  disjxpin  32517  fldextrspunlsplem  33668  sigaclci  34122  fnrelpredd  35079  satfv0  35345  satffunlem2lem1  35391  dmopab3rexdif  35392  elfuns  35903  altopth1  35953  btwnexch2  36011  ifscgr  36032  colinbtwnle  36106  trer  36304  elicc3  36305  bj-imdirval3  37172  bj-finsumval0  37273  difunieq  37362  fvineqsneu  37399  fvineqsneq  37400  poimirlem27  37641  poimir  37647  cnambfre  37662  itg2addnclem2  37666  itg2addnc  37668  areacirclem1  37702  heiborlem4  37808  elghomlem2OLD  37880  rngo2  37901  ispridl2  38032  ispridlc  38064  iss2  38326  membpartlem19  38803  paddasslem14  39827  ispsubcl2N  39941  cdleme29ex  40368  cdlemefr29exN  40396  eldiophss  42762  rencldnfilem  42808  oaabsb  43283  cantnfresb  43313  tfsconcatrn  43331  naddwordnexlem1  43386  clsk1indlem3  44032  ntrneikb  44083  mnuop3d  44260  ax6e2ndeq  44549  suctrALT2  44826  relpmin  44942  relpfrlem  44943  2reu3  47111  iccpartiltu  47423  bgoldbtbndlem2  47807  grtrimap  47947  grimgrtri  47948  isubgr3stgrlem6  47970  isubgr3stgr  47974  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem4  48109  itschlc0xyqsol1  48755  resipos  48963  elsetrecslem  49688  aacllem  49790